Section: New Results

PDSs for translation validation: from SIGNAL to C

Participants : Van-Chan Ngo, Jean-Pierre Talpin, Loïc Besnard.

Synchronous programming languages provide a formal and abstract model of concurrency to facilitate the implementation of concurrent embedded software by automating the most complex tasks of verification, validation and code generation. They also guarantee the reliability of the design/implementation of concurrent embedded software by providing either the proof of compiler's correction or the validation of each run of the compiler. Adopting the translation validation approach [49] , we provide an automatic process to formally verify the code C generation task of the SIGNAL's compiler.

The verification framework will take the SIGNAL program and the generated C code program as the input and proves whether the generated C code correctly implements the SIGNAL program. It also allows to automatically generate the refinement and counterexamples of the generated C code.

Polynomial dynamical system - PDS is used as a common semantic framework to model the behavior of both the SIGNAL program and its generated C code. First, the generated C code is translated into the target SIGNAL program [34] thanks to the intermediate SSA forms. An appropriate relation called refinement for PDSs is proposed to represent the correct implementation relation between the SIGNAL program and its generated C code. The generated code C correctly implements the SIGNAL program if and only if there is a refinement for their PDSs and we say that the generated C code's PDS refines the SIGNAL program's PDS. A proof method which allows to generate the refinement or counterexamples, and then proposes a refining process for the generated C code.